Nuprl Definition : derived-seq
0,22
postcript
pdf
derived-seq(
f
;
s
) ==
s
/
k
,
g
.
n
.<
k
,
i
.
f
(
n
+
g
(
i
))>
latex
Definitions
A
/
x
,
y
.
B
(
x
;
y
)
,
<
a
,
b
>
,
x
.
A
(
x
)
,
n
+
m
,
f
(
a
)
FDL editor aliases
derived-seq
origin
n.<k,i.f(n+g(i))> n.<k,i.f(n+g(i))> x.A(x)